task024 #7
task024 #7
Conversation
tasks/human_eval_024.rs
Outdated
| } | ||
|
|
||
| /// Specification for what it means for d to divide a | ||
| pub open spec fn divides(v: nat, d: nat) -> bool { |
There was a problem hiding this comment.
Can you reverse the ordering of the arguments in divides, so that it matches the English connotation, i.e., so divides(d, v) matches "d divides v"?
There was a problem hiding this comment.
For some reason, one example in verus also follows the less intuitive ordering https://github.com/verus-lang/verus/blob/bbc3e9d68b64f715b62ba46378e859cf0534d1fc/source/rust_verify/example/assorted_demo.rs#L31-L33
|
Also a brief scan on |
Yes, that's somewhere on our to-do list. |
|
PR #8 adds a CI check for verusfmt |
|
Thanks @jaybosamiya! @ahuoguo once you run |
|
i’ve already ran it |
|
Great, thanks! |
I require
n > 1since the python implementation did not take care of arguments outside of it. (It will actually returnNone)